package com.googlecode.kipler.satisfiability.completion.rule.formula.uniformnotation;

import com.googlecode.kipler.syntax.LTLBinaryOperator;
import com.googlecode.kipler.syntax.LTLUnaryOperator;
import com.googlecode.kipler.syntax.formula.BooleanFormula;
import com.googlecode.kipler.syntax.formula.Formula;
import com.googlecode.kipler.syntax.formula.LTLBinaryFormula;
import com.googlecode.kipler.syntax.formula.LTLUnaryFormula;


public class BeforeAlphaFormula implements AlphaFormula {

	private LTLBinaryFormula binFor;

	private Formula alpha1, alpha2;

	private boolean valid;

	public BeforeAlphaFormula() {
		super();
	}

	public BeforeAlphaFormula(Formula Formula) {
		setAlpha(Formula);
	}

	@Override
	public void setAlpha(Formula f) {
		valid = false;
		if (f instanceof LTLBinaryFormula) {
			binFor = (LTLBinaryFormula) f;
			if (binFor.getConstructor() == LTLBinaryOperator.BEFORE) {
				alpha1 = binFor.getRhs().copy().toggleNegated();
				alpha2 = new BooleanFormula(BooleanFormula.Operator.OR, binFor
						.getLhs(),
						new LTLUnaryFormula(LTLUnaryOperator.NEXT, f));
				valid = true;
			}
		}
	}

	@Override
	public Formula getAlpha1() {
		return alpha1;
	}

	@Override
	public Formula getAlpha2() {
		return alpha2;
	}

	public boolean isValid() {
		return valid;
	}

}
